|
| 1: |
|
and(false,false) |
→ false |
| 2: |
|
and(true,false) |
→ false |
| 3: |
|
and(false,true) |
→ false |
| 4: |
|
and(true,true) |
→ true |
| 5: |
|
eq(nil,nil) |
→ true |
| 6: |
|
eq(cons(T,L),nil) |
→ false |
| 7: |
|
eq(nil,cons(T,L)) |
→ false |
| 8: |
|
eq(cons(T,L),cons(Tp,Lp)) |
→ and(eq(T,Tp),eq(L,Lp)) |
| 9: |
|
eq(var(L),var(Lp)) |
→ eq(L,Lp) |
| 10: |
|
eq(var(L),apply(T,S)) |
→ false |
| 11: |
|
eq(var(L),lambda(X,T)) |
→ false |
| 12: |
|
eq(apply(T,S),var(L)) |
→ false |
| 13: |
|
eq(apply(T,S),apply(Tp,Sp)) |
→ and(eq(T,Tp),eq(S,Sp)) |
| 14: |
|
eq(apply(T,S),lambda(X,Tp)) |
→ false |
| 15: |
|
eq(lambda(X,T),var(L)) |
→ false |
| 16: |
|
eq(lambda(X,T),apply(Tp,Sp)) |
→ false |
| 17: |
|
eq(lambda(X,T),lambda(Xp,Tp)) |
→ and(eq(T,Tp),eq(X,Xp)) |
| 18: |
|
if(true,var(K),var(L)) |
→ var(K) |
| 19: |
|
if(false,var(K),var(L)) |
→ var(L) |
| 20: |
|
ren(var(L),var(K),var(Lp)) |
→ if(eq(L,Lp),var(K),var(Lp)) |
| 21: |
|
ren(X,Y,apply(T,S)) |
→ apply(ren(X,Y,T),ren(X,Y,S)) |
| 22: |
|
ren(X,Y,lambda(Z,T)) |
→ lambda(var(cons(X,cons(Y,cons(lambda(Z,T),nil)))),ren(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil)))),T))) |
|
There are 16 dependency pairs:
|
| 23: |
|
EQ(cons(T,L),cons(Tp,Lp)) |
→ AND(eq(T,Tp),eq(L,Lp)) |
| 24: |
|
EQ(cons(T,L),cons(Tp,Lp)) |
→ EQ(T,Tp) |
| 25: |
|
EQ(cons(T,L),cons(Tp,Lp)) |
→ EQ(L,Lp) |
| 26: |
|
EQ(var(L),var(Lp)) |
→ EQ(L,Lp) |
| 27: |
|
EQ(apply(T,S),apply(Tp,Sp)) |
→ AND(eq(T,Tp),eq(S,Sp)) |
| 28: |
|
EQ(apply(T,S),apply(Tp,Sp)) |
→ EQ(T,Tp) |
| 29: |
|
EQ(apply(T,S),apply(Tp,Sp)) |
→ EQ(S,Sp) |
| 30: |
|
EQ(lambda(X,T),lambda(Xp,Tp)) |
→ AND(eq(T,Tp),eq(X,Xp)) |
| 31: |
|
EQ(lambda(X,T),lambda(Xp,Tp)) |
→ EQ(T,Tp) |
| 32: |
|
EQ(lambda(X,T),lambda(Xp,Tp)) |
→ EQ(X,Xp) |
| 33: |
|
REN(var(L),var(K),var(Lp)) |
→ IF(eq(L,Lp),var(K),var(Lp)) |
| 34: |
|
REN(var(L),var(K),var(Lp)) |
→ EQ(L,Lp) |
| 35: |
|
REN(X,Y,apply(T,S)) |
→ REN(X,Y,T) |
| 36: |
|
REN(X,Y,apply(T,S)) |
→ REN(X,Y,S) |
| 37: |
|
REN(X,Y,lambda(Z,T)) |
→ REN(X,Y,ren(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil)))),T)) |
| 38: |
|
REN(X,Y,lambda(Z,T)) |
→ REN(Z,var(cons(X,cons(Y,cons(lambda(Z,T),nil)))),T) |
|
The approximated dependency graph contains 2 SCCs:
{24-26,28,29,31,32}
and {35-38}.